Verification of safety critical software is a difficult problem—with associated large amounts of time and cost. Model-based development (MBD) tools are widely used to specify algorithms for control systems (such as flight controls, engine controls, navigation, etc.) so that tests can be automatically created to verify that the implementation of the block diagrams in the control systems correctly implements the specified algorithms. This automation of test generation has great potential for significantly reducing the verification cost and time; especially when the tests are generated to test for the specific “algorithm requirements” implied by the semantics of a data-flow or statechart diagram.
In an MBD tool modeling notation, an algorithm may be specified by a data-flow block diagram, a statechart, or a combination diagram where statecharts are embedded as data-flow blocks in a data-flow diagram (or vice versa). More generally, a “hybrid diagram” is a diagram where two or more types of semantic notation are used, such as data-flow notation, statechart notation, and/or sequence diagram notation. Requirements-driven test generation techniques have been proposed and implemented for pure data-flow diagrams and pure statecharts.
The algorithm may be expressed using a “diagram” made up of “nodes” and “arcs”. A diagram may be described textually and/or pictorially. A node in a diagram may also contain an internal diagram. The internal diagram can be referred to as a sub-diagram, where each sub-diagram may be comprises of nodes that have internal diagrams or sub-sub-diagrams, and so on. Typically, this hierarchy of diagram, sub-diagram, sub-sub-diagram, etc. is expressed in parent/child relationship terms. Generally speaking, any given node (or set of nodes) within the diagram may have ancestors, including a parent diagram, that ultimately lead up to the top-level diagram. Also, the given node may have child sub-diagram(s), sub-sub-diagram(s), etc. as well. As a special case, the top-level diagram may be thought of as the ultimate parent diagram. A top-level diagram may also be called a model.
A data-flow diagram is a directed, possibly cyclic, diagram where each node in the diagram performs some type of function, and the arcs connecting nodes indicate how data flow from one node to another. A node of the data flow diagram is also called a “block”, and each block has a block type. Blocks may have multiple incoming arcs and multiple outgoing arcs. Each end of an arc is connected to a block via a “port”. Ports are unidirectional—information either flows in or out, but not both. An “input port” may have at most one incoming arc, but an “output port” can have an unlimited number of outgoing arcs. Blocks without incoming arcs are considered “input blocks” and blocks without outgoing arcs are considered “output blocks”.
A statechart is a directed, possibly cyclic, diagram that comprises a plurality of nodes called “states” and a plurality of arcs called “transitions”, each of which indicates a path from a source state to a destination state. Each transition may comprise one or more “conditions” or prerequisites that must be satisfied before traversing the transition. Each state may specify one or more “statechart-defined variables” which are used within the statechart to store a value. A statechart may comprise one or more “statechart-input variables”, or values provided to the device before performing the system function, and one or more “statechart-output variables”, or values output by the device after performing the system function. Each condition may be expressed in terms of the statechart-defined variables, the statechart-input variables and/or the statechart-output variables.
A sequence diagram is a directed diagram that presents an interaction, or a set of arcs called “messages” between a set of nodes called “objects” to effect a desired operation or result. The sequence diagram has two dimensions: a time dimension (typically a vertical axis) and an object dimension (typically a horizontal axis). As the time dimension normally proceeds down the vertical axis, messages that occur later in time often are shown in sequence diagrams as below earlier messages. There is no significance to the ordering of messages along the object dimension.
Hybrid diagrams may be useful to specify requirements for a device or system naturally specified in terms of multiple semantic notations. For example, a cruise control device for an automobile may naturally be described as having states, such as “cruise control engaged”, “cruise control accelerating”, “cruise control decelerating”, “cruise control disengaged”, etc. The information within each state may be modeled using a data flow technique that indicates how information streams between program modules, tasks, processes, or threads that implement the state, such as indicating that a “desired speed” value may be set by a “cruise_control_UI” user interface thread and read by a “cruise_control_engine_interface” engine interface thread to determine if the automobile should accelerate, decelerate, or maintain speed.
For hybrid diagrams, however, the current state-of-the-art comprises two main approaches. The first approach is to transform the hybrid diagram using a lower-level notation that supports both the dataflow and statechart semantics. For example, current model checker tools transform the diagram using a lower-level notation, such as a program-counter and variable-state notation. The second approach is to generate random values for the inputs of the diagram and to compute the expected output values through hybrid model simulation.